What

Hardening follow-up to the L10 echo-residue work — fully in-site (local verification; CI billing remains blocked, so this was the "continue in-site" path). Two things:

1. Gate the L10 proofs in the canonical proof suite

The Layer-10 echo-types proofs were checked only ad-hoc (idris2 --check) outside the gated suite. They're now first-class entries in audits/canonical-proof-suite/MANIFEST.a2ml, getting the same nightly enforcement as the M/S/E classics — a new language domain:

37 entries total; manifest paren-balanced (490/490); the runner's own awk parses both with the correct prover/path/symbol.

Subtle fix: the runner's scan_banned is a whole-file substring match (grep -qF), so the two files' own "zero believe_me / assert_total / sorry" disclaimer comments would have false-flagged them as stub. Reworded those four comment lines to "no escape hatches" phrasing — meaning preserved, banned tokens gone.

Verified locally exactly as the runner invokes (it cds into the file's dir and checks the basename, so module EchoResidue matches EchoResidue.idr):

• idris2 --check → exit 0 for both
• banned-construct scan → 0 hits
• verify_idris2_symbol (signature + clause) → PASS for both headlines

REPORT.a2ml is intentionally not regenerated here: this host has no Rocq 9, so a local run would falsely downgrade the ~30 rocq entries — the nightly suite regenerates it with the full toolchain.

2. End-to-end example

examples/named_reversibility.007 exercises reversible as <name> / reverse <name> through the whole pipeline. Built oo7 and ran the e2e sections:

• oo7 parse → PASS
• oo7 check → PASS (type check passed)
• oo7 run → PASS

Verification

banned scan         : 0 tokens (both files)
idris2 --check      : exit 0 (both, runner-style cd+basename)
symbol sig+clause   : PASS (reverseAfterIrreversibleIllTyped, reverseLinear)
manifest            : 37 entries, parens balanced, awk-parse clean
example e2e         : parse + check + run all PASS
A2ML 6a2            : 0 errors

Scope

Pure hardening — no compiler/grammar/typechecker changes (rung 3a already merged in #42). 7 files: manifest + 2 proof comment rewords + example + CHANGELOG + STATE + session-log.

CI is still gated by the Actions billing/spending-limit rejection (account-owner action); everything above was verified locally.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

Generated by Claude Code